Inference at * 1 1 0 
Iof proof for Lemma bnot of le int:



1. i : 
2. j : 
  (j <z i) = j <z i 

latex

 by PERMUTE{1:n, 2:n, 3:n, 3:n} 

latex

 1: .....wf..... NILNIL

 1:    = 
 2: .....wf..... NILNIL

 2:   j <z i  
 3: .....wf..... NILNIL

 3:   j <z i = j <z i
 .

Definitions	t  T, x:A  B(x), f(a), x:AB(x), Type, i <z j, b, , s = t, , x:A. B(x), P  Q, P  Q, P  Q, P  Q
Lemmas	bnot bnot elim